package fst.calculi.STLC

import fst.binding.Binding

trait Syntax extends Binding {
  trait Node {
    def prettyPrint: String = toString
  }
  
  sealed trait Term extends Node with Nominal[Term] {
    def isValue: Boolean
  }

  case class Var(name: Name) extends Term {
    def isValue = false

    def swap(a: Name, b: Name) = Var(name swap(a, b))
    def fresh(a: Name) = name fresh(a)
    def alphaEq(o: AlsoNominal[Term]) = o match {
      case Var(n) => n.alphaEq(name)
      case _ => false
    }
  }

  case class Abs(tp: Type, abs: \\[Term]) extends Term {
    def isValue = true

    def swap(a: Name, b: Name) =  Abs(tp, abs swap(a, b))
    def fresh(a: Name) = abs fresh(a)
    def alphaEq(o: AlsoNominal[Term]) = o match {
      case Abs(t, a) => t == tp && a.alphaEq(abs)
      case _ => false
    }    
  }

  case class App(fun: Term, arg: Term) extends Term {
    def isValue = false

    def swap(a: Name, b: Name) = App(fun swap(a, b), arg  swap(a, b))
    def fresh(a: Name) = fun.fresh(a) && arg.fresh(a)
    def alphaEq(o: AlsoNominal[Term]) = o match {
      case App(f, a) => f.alphaEq(fun) && a.alphaEq(arg)
      case _ => false
    }    
  }

  class Literal extends Term { 
    def isValue = true 
    def swap(a: Name, b: Name) = this
    def fresh(a: Name) = true    
    def alphaEq(o: AlsoNominal[Term]) = o == this
  }
  case object LTrue extends Literal
  case object LFalse extends Literal
  
  sealed trait Type extends Node
  
  case class TArr(from: Type, to: Type) extends Type
  case object TBool extends Type
}

trait Substitution extends Syntax {
  def subst(self: Term, n: Name, to: Term): Term = self match{
    case Var(name) => if(name.alphaEq(n)) to else self
    case App(fun, arg) => App(subst(fun, n, to), 
                            subst(arg, n, to))
    case Abs(tp, \\(x, body)) => Abs(tp, \\(x, subst(body, n, to)))
    case _ : Literal => self
  }
}